FDL - Nuprl Definition : l_member

Nuprl Definition : l_member

(x

l) ==

i:

. ((i < ||l||) c

(x = l[i]))

clarification:

(x

l

T) ==

i:

. ((i < ||l||) c

(x = l[i]

T))

Definitions x:A. B(x), , A c B, a < b, ||as||, s = t, l[i]

FDL editor aliases l_member